$\forall$$A$:Type, ${\it eq}$:EqDecider($A$), $x$,$y$:$A$, $v$:top.
\\[0ex]sqequal(fpf{-}dom(${\it eq}$; $x$; fpf{-}single($y$; $v$)); (eqof(${\it eq}$)($y$,$x$)))